/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Order.CompleteLattice
import Mathlib.Order.Synonym
import Mathlib.Order.Hom.Set
import Mathlib.Order.Bounds.Basic

#align_import order.galois_connection from "leanprover-community/mathlib"@"c5c7e2760814660967bc27f0de95d190a22297f3"

/-!
# Galois connections, insertions and coinsertions

Galois connections are order theoretic adjoints, i.e. a pair of functions `u` and `l`,
such that `∀ a b, l a ≤ b ↔ a ≤ u b`.

## Main definitions

* `GaloisConnection`: A Galois connection is a pair of functions `l` and `u` satisfying
  `l a ≤ b ↔ a ≤ u b`. They are special cases of adjoint functors in category theory,
  but do not depend on the category theory library in mathlib.
* `GaloisInsertion`: A Galois insertion is a Galois connection where `l ∘ u = id`
* `GaloisCoinsertion`: A Galois coinsertion is a Galois connection where `u ∘ l = id`

## Implementation details

Galois insertions can be used to lift order structures from one type to another.
For example, if `α` is a complete lattice, and `l : α → β` and `u : β → α` form a Galois insertion,
then `β` is also a complete lattice. `l` is the lower adjoint and `u` is the upper adjoint.

An example of a Galois insertion is in group theory. If `G` is a group, then there is a Galois
insertion between the set of subsets of `G`, `Set G`, and the set of subgroups of `G`,
`Subgroup G`. The lower adjoint is `Subgroup.closure`, taking the `Subgroup` generated by a `Set`,
and the upper adjoint is the coercion from `Subgroup G` to `Set G`, taking the underlying set
of a subgroup.

Naively lifting a lattice structure along this Galois insertion would mean that the definition
of `inf` on subgroups would be `Subgroup.closure (↑S ∩ ↑T)`. This is an undesirable definition
because the intersection of subgroups is already a subgroup, so there is no need to take the
closure. For this reason a `choice` function is added as a field to the `GaloisInsertion`
structure. It has type `Π S : Set G, ↑(closure S) ≤ S → Subgroup G`. When `↑(closure S) ≤ S`, then
`S` is already a subgroup, so this function can be defined using `Subgroup.mk` and not `closure`.
This means the infimum of subgroups will be defined to be the intersection of sets, paired
with a proof that intersection of subgroups is a subgroup, rather than the closure of the
intersection.
-/


open Function OrderDual Set

universe u v w x

variable {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {κ : ι → Sort*} {a a₁ a₂ : α}
  {b b₁ b₂ : β}

/-- A Galois connection is a pair of functions `l` and `u` satisfying
`l a ≤ b ↔ a ≤ u b`. They are special cases of adjoint functors in category theory,
but do not depend on the category theory library in mathlib. -/
def GaloisConnection [Preorder α] [Preorder β] (l : α → β) (u : β → α) :=
  ∀ a b, l a ≤ b ↔ a ≤ u b
#align galois_connection GaloisConnection

/-- Makes a Galois connection from an order-preserving bijection. -/
theorem OrderIso.to_galoisConnection [Preorder α] [Preorder β] (oi : α ≃o β) :
    GaloisConnection oi oi.symm := fun _ _ => oi.rel_symm_apply.symm
#align order_iso.to_galois_connection OrderIso.to_galoisConnection

namespace GaloisConnection

section

variable [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a))
    (hlu : ∀ a, l (u a) ≤ a) : GaloisConnection l u := fun _ _ =>
  ⟨fun h => (hul _).trans (hu h), fun h => (hl h).trans (hlu _)⟩
#align galois_connection.monotone_intro GaloisConnection.monotone_intro

protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    GaloisConnection (OrderDual.toDual ∘ u ∘ OrderDual.ofDual)
      (OrderDual.toDual ∘ l ∘ OrderDual.ofDual) :=
  fun a b => (gc b a).symm
#align galois_connection.dual GaloisConnection.dual

theorem le_iff_le {a : α} {b : β} : l a ≤ b ↔ a ≤ u b :=
  gc _ _
#align galois_connection.le_iff_le GaloisConnection.le_iff_le

theorem l_le {a : α} {b : β} : a ≤ u b → l a ≤ b :=
  (gc _ _).mpr
#align galois_connection.l_le GaloisConnection.l_le

theorem le_u {a : α} {b : β} : l a ≤ b → a ≤ u b :=
  (gc _ _).mp
#align galois_connection.le_u GaloisConnection.le_u

theorem le_u_l (a) : a ≤ u (l a) :=
  gc.le_u <| le_rfl
#align galois_connection.le_u_l GaloisConnection.le_u_l

theorem l_u_le (a) : l (u a) ≤ a :=
  gc.l_le <| le_rfl
#align galois_connection.l_u_le GaloisConnection.l_u_le

theorem monotone_u : Monotone u := fun a _ H => gc.le_u ((gc.l_u_le a).trans H)
#align galois_connection.monotone_u GaloisConnection.monotone_u

theorem monotone_l : Monotone l :=
  gc.dual.monotone_u.dual
#align galois_connection.monotone_l GaloisConnection.monotone_l

theorem upperBounds_l_image (s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s :=
  Set.ext fun b => by simp [upperBounds, gc _ _]
#align galois_connection.upper_bounds_l_image GaloisConnection.upperBounds_l_image

theorem lowerBounds_u_image (s : Set β) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s :=
  gc.dual.upperBounds_l_image s
#align galois_connection.lower_bounds_u_image GaloisConnection.lowerBounds_u_image

theorem bddAbove_l_image {s : Set α} : BddAbove (l '' s) ↔ BddAbove s :=
  ⟨fun ⟨x, hx⟩ => ⟨u x, by rwa [gc.upperBounds_l_image] at hx⟩, gc.monotone_l.map_bddAbove⟩
#align galois_connection.bdd_above_l_image GaloisConnection.bddAbove_l_image

theorem bddBelow_u_image {s : Set β} : BddBelow (u '' s) ↔ BddBelow s :=
  gc.dual.bddAbove_l_image
#align galois_connection.bdd_below_u_image GaloisConnection.bddBelow_u_image

theorem isLUB_l_image {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a) :=
  ⟨gc.monotone_l.mem_upperBounds_image h.left, fun b hb =>
    gc.l_le <| h.right <| by rwa [gc.upperBounds_l_image] at hb⟩
#align galois_connection.is_lub_l_image GaloisConnection.isLUB_l_image

theorem isGLB_u_image {s : Set β} {b : β} (h : IsGLB s b) : IsGLB (u '' s) (u b) :=
  gc.dual.isLUB_l_image h
#align galois_connection.is_glb_u_image GaloisConnection.isGLB_u_image

theorem isLeast_l {a : α} : IsLeast { b | a ≤ u b } (l a) :=
  ⟨gc.le_u_l _, fun _ hb => gc.l_le hb⟩
#align galois_connection.is_least_l GaloisConnection.isLeast_l

theorem isGreatest_u {b : β} : IsGreatest { a | l a ≤ b } (u b) :=
  gc.dual.isLeast_l
#align galois_connection.is_greatest_u GaloisConnection.isGreatest_u

theorem isGLB_l {a : α} : IsGLB { b | a ≤ u b } (l a) :=
  gc.isLeast_l.isGLB
#align galois_connection.is_glb_l GaloisConnection.isGLB_l

theorem isLUB_u {b : β} : IsLUB { a | l a ≤ b } (u b) :=
  gc.isGreatest_u.isLUB
#align galois_connection.is_lub_u GaloisConnection.isLUB_u

/-- If `(l, u)` is a Galois connection, then the relation `x ≤ u (l y)` is a transitive relation.
If `l` is a closure operator (`Submodule.span`, `Subgroup.closure`, ...) and `u` is the coercion to
`Set`, this reads as "if `U` is in the closure of `V` and `V` is in the closure of `W` then `U` is
in the closure of `W`". -/
theorem le_u_l_trans {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z) :=
  hxy.trans (gc.monotone_u <| gc.l_le hyz)
#align galois_connection.le_u_l_trans GaloisConnection.le_u_l_trans

theorem l_u_le_trans {x y z : β} (hxy : l (u x) ≤ y) (hyz : l (u y) ≤ z) : l (u x) ≤ z :=
  (gc.monotone_l <| gc.le_u hxy).trans hyz
#align galois_connection.l_u_le_trans GaloisConnection.l_u_le_trans

end

section PartialOrder

variable [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem u_l_u_eq_u (b : β) : u (l (u b)) = u b :=
  (gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)
#align galois_connection.u_l_u_eq_u GaloisConnection.u_l_u_eq_u

theorem u_l_u_eq_u' : u ∘ l ∘ u = u :=
  funext gc.u_l_u_eq_u
#align galois_connection.u_l_u_eq_u' GaloisConnection.u_l_u_eq_u'

theorem u_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ a, l a = l' a)
    {b : β} : u b = u' b :=
  le_antisymm (gc'.le_u <| hl (u b) ▸ gc.l_u_le _) (gc.le_u <| (hl (u' b)).symm ▸ gc'.l_u_le _)
#align galois_connection.u_unique GaloisConnection.u_unique

/-- If there exists a `b` such that `a = u a`, then `b = l a` is one such element. -/
theorem exists_eq_u (a : α) : (∃ b : β, a = u b) ↔ a = u (l a) :=
  ⟨fun ⟨_, hS⟩ => hS.symm ▸ (gc.u_l_u_eq_u _).symm, fun HI => ⟨_, HI⟩⟩
#align galois_connection.exists_eq_u GaloisConnection.exists_eq_u

theorem u_eq {z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y := by
  constructor
  · rintro rfl x
    exact (gc x y).symm
  · intro H
    exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)
#align galois_connection.u_eq GaloisConnection.u_eq

end PartialOrder

section PartialOrder

variable [Preorder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem l_u_l_eq_l (a : α) : l (u (l a)) = l a := gc.dual.u_l_u_eq_u _
#align galois_connection.l_u_l_eq_l GaloisConnection.l_u_l_eq_l

theorem l_u_l_eq_l' : l ∘ u ∘ l = l := funext gc.l_u_l_eq_l
#align galois_connection.l_u_l_eq_l' GaloisConnection.l_u_l_eq_l'

theorem l_unique {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ b, u b = u' b)
    {a : α} : l a = l' a :=
  gc.dual.u_unique gc'.dual hu
#align galois_connection.l_unique GaloisConnection.l_unique

/-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/
theorem exists_eq_l (b : β) : (∃ a : α, b = l a) ↔ b = l (u b) := gc.dual.exists_eq_u _
#align galois_connection.exists_eq_l GaloisConnection.exists_eq_l

theorem l_eq {x : α} {z : β} : l x = z ↔ ∀ y, z ≤ y ↔ x ≤ u y := gc.dual.u_eq
#align galois_connection.l_eq GaloisConnection.l_eq

end PartialOrder

section OrderTop

variable [PartialOrder α] [Preorder β] [OrderTop α]

theorem u_eq_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : u x = ⊤ ↔ l ⊤ ≤ x :=
  top_le_iff.symm.trans gc.le_iff_le.symm
#align galois_connection.u_eq_top GaloisConnection.u_eq_top

theorem u_top [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤ :=
  gc.u_eq_top.2 le_top
#align galois_connection.u_top GaloisConnection.u_top

end OrderTop

section OrderBot

variable [Preorder α] [PartialOrder β] [OrderBot β]

theorem l_eq_bot {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : l x = ⊥ ↔ x ≤ u ⊥ :=
  gc.dual.u_eq_top
#align galois_connection.l_eq_bot GaloisConnection.l_eq_bot

theorem l_bot [OrderBot α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥ :=
  gc.dual.u_top
#align galois_connection.l_bot GaloisConnection.l_bot

end OrderBot

section SemilatticeSup

variable [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem l_sup : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂ :=
  (gc.isLUB_l_image isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]
#align galois_connection.l_sup GaloisConnection.l_sup

end SemilatticeSup

section SemilatticeInf

variable [SemilatticeInf α] [SemilatticeInf β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem u_inf : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂ := gc.dual.l_sup
#align galois_connection.u_inf GaloisConnection.u_inf

end SemilatticeInf

section CompleteLattice

variable [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem l_iSup {f : ι → α} : l (iSup f) = ⨆ i, l (f i) :=
  Eq.symm <|
    IsLUB.iSup_eq <|
      show IsLUB (range (l ∘ f)) (l (iSup f)) by
        rw [range_comp, ← sSup_range]; exact gc.isLUB_l_image (isLUB_sSup _)
#align galois_connection.l_supr GaloisConnection.l_iSup

theorem l_iSup₂ {f : ∀ i, κ i → α} : l (⨆ (i) (j), f i j) = ⨆ (i) (j), l (f i j) := by
  simp_rw [gc.l_iSup]
#align galois_connection.l_supr₂ GaloisConnection.l_iSup₂

theorem u_iInf {f : ι → β} : u (iInf f) = ⨅ i, u (f i) :=
  gc.dual.l_iSup
#align galois_connection.u_infi GaloisConnection.u_iInf

theorem u_iInf₂ {f : ∀ i, κ i → β} : u (⨅ (i) (j), f i j) = ⨅ (i) (j), u (f i j) :=
  gc.dual.l_iSup₂
#align galois_connection.u_infi₂ GaloisConnection.u_iInf₂

theorem l_sSup {s : Set α} : l (sSup s) = ⨆ a ∈ s, l a := by simp only [sSup_eq_iSup, gc.l_iSup]
#align galois_connection.l_Sup GaloisConnection.l_sSup

theorem u_sInf {s : Set β} : u (sInf s) = ⨅ a ∈ s, u a :=
  gc.dual.l_sSup
#align galois_connection.u_Inf GaloisConnection.u_sInf

end CompleteLattice

section LinearOrder

variable [LinearOrder α] [LinearOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u)

theorem lt_iff_lt {a : α} {b : β} : b < l a ↔ u b < a :=
  lt_iff_lt_of_le_iff_le (gc a b)
#align galois_connection.lt_iff_lt GaloisConnection.lt_iff_lt

end LinearOrder

-- Constructing Galois connections
section Constructions

protected theorem id [pα : Preorder α] : @GaloisConnection α α pα pα id id := fun _ _ =>
  Iff.intro (fun x => x) fun x => x
#align galois_connection.id GaloisConnection.id

protected theorem compose [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α}
    {l2 : β → γ} {u2 : γ → β} (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) :
    GaloisConnection (l2 ∘ l1) (u1 ∘ u2) := fun _ _ ↦ (gc2 _ _).trans (gc1 _ _)
#align galois_connection.compose GaloisConnection.compose

protected theorem dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w} [∀ i, Preorder (α i)]
    [∀ i, Preorder (β i)] (l : ∀ i, α i → β i) (u : ∀ i, β i → α i)
    (gc : ∀ i, GaloisConnection (l i) (u i)) :
    GaloisConnection (fun (a : ∀ i, α i) i => l i (a i)) fun b i => u i (b i) := fun a b =>
  forall_congr' fun i => gc i (a i) (b i)
#align galois_connection.dfun GaloisConnection.dfun

protected theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) :
    GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := fun a b ↦ by
  dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

end Constructions

theorem l_comm_of_u_comm {X : Type*} [Preorder X] {Y : Type*} [Preorder Y] {Z : Type*}
    [Preorder Z] {W : Type*} [PartialOrder W] {lYX : X → Y} {uXY : Y → X}
    (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW)
    {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X}
    (hXZ : GaloisConnection lZX uXZ) (h : ∀ w, uXZ (uZW w) = uXY (uYW w)) {x : X} :
    lWZ (lZX x) = lWY (lYX x) :=
  (hXZ.compose hZW).l_unique (hXY.compose hWY) h
#align galois_connection.l_comm_of_u_comm GaloisConnection.l_comm_of_u_comm

theorem u_comm_of_l_comm {X : Type*} [PartialOrder X] {Y : Type*} [Preorder Y] {Z : Type*}
    [Preorder Z] {W : Type*} [Preorder W] {lYX : X → Y} {uXY : Y → X}
    (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW)
    {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X}
    (hXZ : GaloisConnection lZX uXZ) (h : ∀ x, lWZ (lZX x) = lWY (lYX x)) {w : W} :
    uXZ (uZW w) = uXY (uYW w) :=
  (hXZ.compose hZW).u_unique (hXY.compose hWY) h
#align galois_connection.u_comm_of_l_comm GaloisConnection.u_comm_of_l_comm

theorem l_comm_iff_u_comm {X : Type*} [PartialOrder X] {Y : Type*} [Preorder Y] {Z : Type*}
    [Preorder Z] {W : Type*} [PartialOrder W] {lYX : X → Y} {uXY : Y → X}
    (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW)
    {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X}
    (hXZ : GaloisConnection lZX uXZ) :
    (∀ w : W, uXZ (uZW w) = uXY (uYW w)) ↔ ∀ x : X, lWZ (lZX x) = lWY (lYX x) :=
  ⟨hXY.l_comm_of_u_comm hZW hWY hXZ, hXY.u_comm_of_l_comm hZW hWY hXZ⟩
#align galois_connection.l_comm_iff_u_comm GaloisConnection.l_comm_iff_u_comm

end GaloisConnection

section

/-- `sSup` and `Iic` form a Galois connection. -/
theorem gc_sSup_Iic [CompleteSemilatticeSup α] :
    GaloisConnection (sSup : Set α → α) (Iic : α → Set α) :=
  fun _ _ ↦ sSup_le_iff

/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois connection. -/
theorem gc_Ici_sInf [CompleteSemilatticeInf α] :
    GaloisConnection (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α) :=
  fun _ _ ↦ le_sInf_iff.symm

variable [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {f : α → β → γ} {s : Set α}
  {t : Set β} {l u : α → β → γ} {l₁ u₁ : β → γ → α} {l₂ u₂ : α → γ → β}

theorem sSup_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sSup s) (sSup t) := by
  simp_rw [sSup_image2, ← (h₂ _).l_sSup, ← (h₁ _).l_sSup]
#align Sup_image2_eq_Sup_Sup sSup_image2_eq_sSup_sSup

theorem sSup_image2_eq_sSup_sInf (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) :
    sSup (image2 l s t) = l (sSup s) (sInf t) :=
  sSup_image2_eq_sSup_sSup (β := βᵒᵈ) h₁ h₂
#align Sup_image2_eq_Sup_Inf sSup_image2_eq_sSup_sInf

theorem sSup_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) : sSup (image2 l s t) = l (sInf s) (sSup t) :=
  sSup_image2_eq_sSup_sSup (α := αᵒᵈ) h₁ h₂
#align Sup_image2_eq_Inf_Sup sSup_image2_eq_sInf_sSup

theorem sSup_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) :
    sSup (image2 l s t) = l (sInf s) (sInf t) :=
  sSup_image2_eq_sSup_sSup (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂
#align Sup_image2_eq_Inf_Inf sSup_image2_eq_sInf_sInf

theorem sInf_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t) := by
  simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]
#align Inf_image2_eq_Inf_Inf sInf_image2_eq_sInf_sInf

theorem sInf_image2_eq_sInf_sSup (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) :
    sInf (image2 u s t) = u (sInf s) (sSup t) :=
  sInf_image2_eq_sInf_sInf (β := βᵒᵈ) h₁ h₂
#align Inf_image2_eq_Inf_Sup sInf_image2_eq_sInf_sSup

theorem sInf_image2_eq_sSup_sInf (h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sSup s) (sInf t) :=
  sInf_image2_eq_sInf_sInf (α := αᵒᵈ) h₁ h₂
#align Inf_image2_eq_Sup_Inf sInf_image2_eq_sSup_sInf

theorem sInf_image2_eq_sSup_sSup (h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) :
    sInf (image2 u s t) = u (sSup s) (sSup t) :=
  sInf_image2_eq_sInf_sInf (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂
#align Inf_image2_eq_Sup_Sup sInf_image2_eq_sSup_sSup

end

namespace OrderIso

variable [Preorder α] [Preorder β]

@[simp]
theorem bddAbove_image (e : α ≃o β) {s : Set α} : BddAbove (e '' s) ↔ BddAbove s :=
  e.to_galoisConnection.bddAbove_l_image
#align order_iso.bdd_above_image OrderIso.bddAbove_image

@[simp]
theorem bddBelow_image (e : α ≃o β) {s : Set α} : BddBelow (e '' s) ↔ BddBelow s :=
  e.dual.bddAbove_image
#align order_iso.bdd_below_image OrderIso.bddBelow_image

@[simp]
theorem bddAbove_preimage (e : α ≃o β) {s : Set β} : BddAbove (e ⁻¹' s) ↔ BddAbove s := by
  rw [← e.bddAbove_image, e.image_preimage]
#align order_iso.bdd_above_preimage OrderIso.bddAbove_preimage

@[simp]
theorem bddBelow_preimage (e : α ≃o β) {s : Set β} : BddBelow (e ⁻¹' s) ↔ BddBelow s := by
  rw [← e.bddBelow_image, e.image_preimage]
#align order_iso.bdd_below_preimage OrderIso.bddBelow_preimage

end OrderIso

namespace Nat

theorem galoisConnection_mul_div {k : ℕ} (h : 0 < k) :
    GaloisConnection (fun n => n * k) fun n => n / k := fun _ _ => (le_div_iff_mul_le h).symm
#align nat.galois_connection_mul_div Nat.galoisConnection_mul_div

end Nat

-- Porting note(#5171): this used to have a `@[nolint has_nonempty_instance]`
/-- A Galois insertion is a Galois connection where `l ∘ u = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual
to `GaloisCoinsertion` -/
structure GaloisInsertion {α β : Type*} [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
  /-- A contructive choice function for images of `l`. -/
  choice : ∀ x : α, u (l x) ≤ x → β
  /-- The Galois connection associated to a Galois insertion. -/
  gc : GaloisConnection l u
  /-- Main property of a Galois insertion. -/
  le_l_u : ∀ x, x ≤ l (u x)
  /-- Property of the choice function. -/
  choice_eq : ∀ a h, choice a h = l a
#align galois_insertion GaloisInsertion

/-- A constructor for a Galois insertion with the trivial `choice` function. -/
def GaloisInsertion.monotoneIntro {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α}
    (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ b, l (u b) = b) :
    GaloisInsertion l u where
  choice x _ := l x
  gc := GaloisConnection.monotone_intro hu hl hul fun b => le_of_eq (hlu b)
  le_l_u b := le_of_eq <| (hlu b).symm
  choice_eq _ _ := rfl
#align galois_insertion.monotone_intro GaloisInsertion.monotoneIntro

/-- Makes a Galois insertion from an order-preserving bijection. -/
protected def OrderIso.toGaloisInsertion [Preorder α] [Preorder β] (oi : α ≃o β) :
    GaloisInsertion oi oi.symm where
  choice b _ := oi b
  gc := oi.to_galoisConnection
  le_l_u g := le_of_eq (oi.right_inv g).symm
  choice_eq _ _ := rfl
#align order_iso.to_galois_insertion OrderIso.toGaloisInsertion

/-- Make a `GaloisInsertion l u` from a `GaloisConnection l u` such that `∀ b, b ≤ l (u b)` -/
def GaloisConnection.toGaloisInsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
    {u : β → α} (gc : GaloisConnection l u) (h : ∀ b, b ≤ l (u b)) : GaloisInsertion l u :=
  { choice := fun x _ => l x
    gc
    le_l_u := h
    choice_eq := fun _ _ => rfl }
#align galois_connection.to_galois_insertion GaloisConnection.toGaloisInsertion

/-- Lift the bottom along a Galois connection -/
def GaloisConnection.liftOrderBot {α β : Type*} [Preorder α] [OrderBot α] [PartialOrder β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    OrderBot β where
  bot := l ⊥
  bot_le _ := gc.l_le <| bot_le
#align galois_connection.lift_order_bot GaloisConnection.liftOrderBot

namespace GaloisInsertion

variable {l : α → β} {u : β → α}

theorem l_u_eq [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b :=
  (gi.gc.l_u_le _).antisymm (gi.le_l_u _)
#align galois_insertion.l_u_eq GaloisInsertion.l_u_eq

theorem leftInverse_l_u [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) :
    LeftInverse l u :=
  gi.l_u_eq
#align galois_insertion.left_inverse_l_u GaloisInsertion.leftInverse_l_u

theorem l_top [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β]
    (gi : GaloisInsertion l u) : l ⊤ = ⊤ :=
  top_unique <| (gi.le_l_u _).trans <| gi.gc.monotone_l le_top

theorem l_surjective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Surjective l :=
  gi.leftInverse_l_u.surjective
#align galois_insertion.l_surjective GaloisInsertion.l_surjective

theorem u_injective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Injective u :=
  gi.leftInverse_l_u.injective
#align galois_insertion.u_injective GaloisInsertion.u_injective

theorem l_sup_u [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊔ u b) = a ⊔ b :=
  calc
    l (u a ⊔ u b) = l (u a) ⊔ l (u b) := gi.gc.l_sup
    _ = a ⊔ b := by simp only [gi.l_u_eq]
#align galois_insertion.l_sup_u GaloisInsertion.l_sup_u

theorem l_iSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    (f : ι → β) : l (⨆ i, u (f i)) = ⨆ i, f i :=
  calc
    l (⨆ i : ι, u (f i)) = ⨆ i : ι, l (u (f i)) := gi.gc.l_iSup
    _ = ⨆ i : ι, f i := congr_arg _ <| funext fun i => gi.l_u_eq (f i)
#align galois_insertion.l_supr_u GaloisInsertion.l_iSup_u

theorem l_biSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ i, p i → β) : l (⨆ (i) (hi), u (f i hi)) = ⨆ (i) (hi), f i hi := by
  simp only [iSup_subtype', gi.l_iSup_u]
#align galois_insertion.l_bsupr_u GaloisInsertion.l_biSup_u

theorem l_sSup_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sSup (u '' s)) = sSup s := by rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
#align galois_insertion.l_Sup_u_image GaloisInsertion.l_sSup_u_image

theorem l_inf_u [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊓ u b) = a ⊓ b :=
  calc
    l (u a ⊓ u b) = l (u (a ⊓ b)) := congr_arg l gi.gc.u_inf.symm
    _ = a ⊓ b := by simp only [gi.l_u_eq]
#align galois_insertion.l_inf_u GaloisInsertion.l_inf_u

theorem l_iInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    (f : ι → β) : l (⨅ i, u (f i)) = ⨅ i, f i :=
  calc
    l (⨅ i : ι, u (f i)) = l (u (⨅ i : ι, f i)) := congr_arg l gi.gc.u_iInf.symm
    _ = ⨅ i : ι, f i := gi.l_u_eq _
#align galois_insertion.l_infi_u GaloisInsertion.l_iInf_u

theorem l_biInf_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), β) : l (⨅ (i) (hi), u (f i hi)) = ⨅ (i) (hi), f i hi := by
  simp only [iInf_subtype', gi.l_iInf_u]
#align galois_insertion.l_binfi_u GaloisInsertion.l_biInf_u

theorem l_sInf_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    (s : Set β) : l (sInf (u '' s)) = sInf s := by rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
#align galois_insertion.l_Inf_u_image GaloisInsertion.l_sInf_u_image

theorem l_iInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) : l (⨅ i, f i) = ⨅ i, l (f i) :=
  calc
    l (⨅ i, f i) = l (⨅ i : ι, u (l (f i))) := by simp [hf]
    _ = ⨅ i, l (f i) := gi.l_iInf_u _
#align galois_insertion.l_infi_of_ul_eq_self GaloisInsertion.l_iInf_of_ul_eq_self

theorem l_biInf_of_ul_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u)
    {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), α) (hf : ∀ i hi, u (l (f i hi)) = f i hi) :
    l (⨅ (i) (hi), f i hi) = ⨅ (i) (hi), l (f i hi) := by
  rw [iInf_subtype', iInf_subtype']
  exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _
#align galois_insertion.l_binfi_of_ul_eq_self GaloisInsertion.l_biInf_of_ul_eq_self

theorem u_le_u_iff [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b} : u a ≤ u b ↔ a ≤ b :=
  ⟨fun h => (gi.le_l_u _).trans (gi.gc.l_le h), fun h => gi.gc.monotone_u h⟩
#align galois_insertion.u_le_u_iff GaloisInsertion.u_le_u_iff

theorem strictMono_u [Preorder α] [Preorder β] (gi : GaloisInsertion l u) : StrictMono u :=
  strictMono_of_le_iff_le fun _ _ => gi.u_le_u_iff.symm
#align galois_insertion.strict_mono_u GaloisInsertion.strictMono_u

theorem isLUB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
    (hs : IsLUB (u '' s) a) : IsLUB s (l a) :=
  ⟨fun x hx => (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.1 <| mem_image_of_mem _ hx, fun _ hx =>
    gi.gc.l_le <| hs.2 <| gi.gc.monotone_u.mem_upperBounds_image hx⟩
#align galois_insertion.is_lub_of_u_image GaloisInsertion.isLUB_of_u_image

theorem isGLB_of_u_image [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {s : Set β} {a : α}
    (hs : IsGLB (u '' s) a) : IsGLB s (l a) :=
  ⟨fun _ hx => gi.gc.l_le <| hs.1 <| mem_image_of_mem _ hx, fun x hx =>
    (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.2 <| gi.gc.monotone_u.mem_lowerBounds_image hx⟩
#align galois_insertion.is_glb_of_u_image GaloisInsertion.isGLB_of_u_image

section lift

variable [PartialOrder β]

-- See note [reducible non instances]
/-- Lift the suprema along a Galois insertion -/
abbrev liftSemilatticeSup [SemilatticeSup α] (gi : GaloisInsertion l u) : SemilatticeSup β :=
  { ‹PartialOrder β› with
    sup := fun a b => l (u a ⊔ u b)
    le_sup_left := fun a _ => (gi.le_l_u a).trans <| gi.gc.monotone_l <| le_sup_left
    le_sup_right := fun _ b => (gi.le_l_u b).trans <| gi.gc.monotone_l <| le_sup_right
    sup_le := fun a b c hac hbc =>
      gi.gc.l_le <| sup_le (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc) }
#align galois_insertion.lift_semilattice_sup GaloisInsertion.liftSemilatticeSup

-- See note [reducible non instances]
/-- Lift the infima along a Galois insertion -/
abbrev liftSemilatticeInf [SemilatticeInf α] (gi : GaloisInsertion l u) : SemilatticeInf β :=
  { ‹PartialOrder β› with
    inf := fun a b =>
      gi.choice (u a ⊓ u b) <|
        le_inf (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_left)
          (gi.gc.monotone_u <| gi.gc.l_le <| inf_le_right)
    inf_le_left := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_left
    inf_le_right := by simp only [gi.choice_eq]; exact fun a b => gi.gc.l_le inf_le_right
    le_inf := by
      simp only [gi.choice_eq]
      exact fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc) }
#align galois_insertion.lift_semilattice_inf GaloisInsertion.liftSemilatticeInf

-- See note [reducible non instances]
/-- Lift the suprema and infima along a Galois insertion -/
abbrev liftLattice [Lattice α] (gi : GaloisInsertion l u) : Lattice β :=
  { gi.liftSemilatticeSup, gi.liftSemilatticeInf with }
#align galois_insertion.lift_lattice GaloisInsertion.liftLattice

-- See note [reducible non instances]
/-- Lift the top along a Galois insertion -/
abbrev liftOrderTop [Preorder α] [OrderTop α] (gi : GaloisInsertion l u) :
    OrderTop β where
  top := gi.choice ⊤ <| le_top
  le_top := by
    simp only [gi.choice_eq]; exact fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)
#align galois_insertion.lift_order_top GaloisInsertion.liftOrderTop

-- See note [reducible non instances]
/-- Lift the top, bottom, suprema, and infima along a Galois insertion -/
abbrev liftBoundedOrder [Preorder α] [BoundedOrder α] (gi : GaloisInsertion l u) : BoundedOrder β :=
  { gi.liftOrderTop, gi.gc.liftOrderBot with }
#align galois_insertion.lift_bounded_order GaloisInsertion.liftBoundedOrder

-- See note [reducible non instances]
/-- Lift all suprema and infima along a Galois insertion -/
abbrev liftCompleteLattice [CompleteLattice α] (gi : GaloisInsertion l u) : CompleteLattice β :=
  { gi.liftBoundedOrder, gi.liftLattice with
    sSup := fun s => l (sSup (u '' s))
    sSup_le := fun s => (gi.isLUB_of_u_image (isLUB_sSup _)).2
    le_sSup := fun s => (gi.isLUB_of_u_image (isLUB_sSup _)).1
    sInf := fun s =>
      gi.choice (sInf (u '' s)) <|
        (isGLB_sInf _).2 <|
          gi.gc.monotone_u.mem_lowerBounds_image (gi.isGLB_of_u_image <| isGLB_sInf _).1
    sInf_le := fun s => by dsimp; rw [gi.choice_eq]; exact (gi.isGLB_of_u_image (isGLB_sInf _)).1
    le_sInf := fun s => by dsimp; rw [gi.choice_eq]; exact (gi.isGLB_of_u_image (isGLB_sInf _)).2 }
#align galois_insertion.lift_complete_lattice GaloisInsertion.liftCompleteLattice

end lift

end GaloisInsertion

-- Porting note(#5171): this used to have a `@[nolint has_nonempty_instance]`
/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
choice function, to give better definitional equalities when lifting order structures. Dual to
`GaloisInsertion` -/
structure GaloisCoinsertion [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
  /-- A contructive choice function for images of `u`. -/
  choice : ∀ x : β, x ≤ l (u x) → α
  /-- The Galois connection associated to a Galois coinsertion. -/
  gc : GaloisConnection l u
  /-- Main property of a Galois coinsertion. -/
  u_l_le : ∀ x, u (l x) ≤ x
  /-- Property of the choice function. -/
  choice_eq : ∀ a h, choice a h = u a
#align galois_coinsertion GaloisCoinsertion

/-- Make a `GaloisInsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisCoinsertion` between `α` and
`β`. -/
def GaloisCoinsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
    GaloisCoinsertion l u → GaloisInsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
#align galois_coinsertion.dual GaloisCoinsertion.dual

/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between `α` and
`β`. -/
def GaloisInsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
    GaloisInsertion l u → GaloisCoinsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
#align galois_insertion.dual GaloisInsertion.dual

/-- Make a `GaloisInsertion` between `α` and `β` from a `GaloisCoinsertion` between `αᵒᵈ` and
`βᵒᵈ`. -/
def GaloisCoinsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
    GaloisCoinsertion l u → GaloisInsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
#align galois_coinsertion.of_dual GaloisCoinsertion.ofDual

/-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ` and
`βᵒᵈ`. -/
def GaloisInsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
    GaloisInsertion l u → GaloisCoinsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual) :=
  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
#align galois_insertion.of_dual GaloisInsertion.ofDual

/-- Makes a Galois coinsertion from an order-preserving bijection. -/
protected def OrderIso.toGaloisCoinsertion [Preorder α] [Preorder β] (oi : α ≃o β) :
    GaloisCoinsertion oi oi.symm where
  choice b _ := oi.symm b
  gc := oi.to_galoisConnection
  u_l_le g := le_of_eq (oi.left_inv g)
  choice_eq _ _ := rfl
#align order_iso.to_galois_coinsertion OrderIso.toGaloisCoinsertion

/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/
def GaloisCoinsertion.monotoneIntro [Preorder α] [Preorder β] {l : α → β} {u : β → α}
    (hu : Monotone u) (hl : Monotone l) (hlu : ∀ b, l (u b) ≤ b) (hul : ∀ a, u (l a) = a) :
    GaloisCoinsertion l u :=
  (GaloisInsertion.monotoneIntro hl.dual hu.dual hlu hul).ofDual
#align galois_coinsertion.monotone_intro GaloisCoinsertion.monotoneIntro

/-- Make a `GaloisCoinsertion l u` from a `GaloisConnection l u` such that `∀ a, u (l a) ≤ a` -/
def GaloisConnection.toGaloisCoinsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
    {u : β → α} (gc : GaloisConnection l u) (h : ∀ a, u (l a) ≤ a) : GaloisCoinsertion l u :=
  { choice := fun x _ => u x
    gc
    u_l_le := h
    choice_eq := fun _ _ => rfl }
#align galois_connection.to_galois_coinsertion GaloisConnection.toGaloisCoinsertion

/-- Lift the top along a Galois connection -/
def GaloisConnection.liftOrderTop {α β : Type*} [PartialOrder α] [Preorder β] [OrderTop β]
    {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    OrderTop α where
  top := u ⊤
  le_top _ := gc.le_u <| le_top
#align galois_connection.lift_order_top GaloisConnection.liftOrderTop

namespace GaloisCoinsertion

variable {l : α → β} {u : β → α}

theorem u_l_eq [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) (a : α) : u (l a) = a :=
  gi.dual.l_u_eq a
#align galois_coinsertion.u_l_eq GaloisCoinsertion.u_l_eq

theorem u_l_leftInverse [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) :
    LeftInverse u l :=
  gi.u_l_eq
#align galois_coinsertion.u_l_left_inverse GaloisCoinsertion.u_l_leftInverse

theorem u_bot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) :
    u ⊥ = ⊥ :=
  gi.dual.l_top

theorem u_surjective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Surjective u :=
  gi.dual.l_surjective
#align galois_coinsertion.u_surjective GaloisCoinsertion.u_surjective

theorem l_injective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Injective l :=
  gi.dual.u_injective
#align galois_coinsertion.l_injective GaloisCoinsertion.l_injective

theorem u_inf_l [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisCoinsertion l u) (a b : α) :
    u (l a ⊓ l b) = a ⊓ b :=
  gi.dual.l_sup_u a b
#align galois_coinsertion.u_inf_l GaloisCoinsertion.u_inf_l

theorem u_iInf_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    (f : ι → α) : u (⨅ i, l (f i)) = ⨅ i, f i :=
  gi.dual.l_iSup_u _
#align galois_coinsertion.u_infi_l GaloisCoinsertion.u_iInf_l

theorem u_sInf_l_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    (s : Set α) : u (sInf (l '' s)) = sInf s :=
  gi.dual.l_sSup_u_image _
#align galois_coinsertion.u_Inf_l_image GaloisCoinsertion.u_sInf_l_image

theorem u_sup_l [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) (a b : α) :
    u (l a ⊔ l b) = a ⊔ b :=
  gi.dual.l_inf_u _ _
#align galois_coinsertion.u_sup_l GaloisCoinsertion.u_sup_l

theorem u_iSup_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    (f : ι → α) : u (⨆ i, l (f i)) = ⨆ i, f i :=
  gi.dual.l_iInf_u _
#align galois_coinsertion.u_supr_l GaloisCoinsertion.u_iSup_l

theorem u_biSup_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ (i) (_ : p i), α) : u (⨆ (i) (hi), l (f i hi)) = ⨆ (i) (hi), f i hi :=
  gi.dual.l_biInf_u _
#align galois_coinsertion.u_bsupr_l GaloisCoinsertion.u_biSup_l

theorem u_sSup_l_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    (s : Set α) : u (sSup (l '' s)) = sSup s :=
  gi.dual.l_sInf_u_image _
#align galois_coinsertion.u_Sup_l_image GaloisCoinsertion.u_sSup_l_image

theorem u_iSup_of_lu_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    {ι : Sort x} (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) : u (⨆ i, f i) = ⨆ i, u (f i) :=
  gi.dual.l_iInf_of_ul_eq_self _ hf
#align galois_coinsertion.u_supr_of_lu_eq_self GaloisCoinsertion.u_iSup_of_lu_eq_self

theorem u_biSup_of_lu_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u)
    {ι : Sort x} {p : ι → Prop} (f : ∀ (i) (_ : p i), β) (hf : ∀ i hi, l (u (f i hi)) = f i hi) :
    u (⨆ (i) (hi), f i hi) = ⨆ (i) (hi), u (f i hi) :=
  gi.dual.l_biInf_of_ul_eq_self _ hf
#align galois_coinsertion.u_bsupr_of_lu_eq_self GaloisCoinsertion.u_biSup_of_lu_eq_self

theorem l_le_l_iff [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {a b} :
    l a ≤ l b ↔ a ≤ b :=
  gi.dual.u_le_u_iff
#align galois_coinsertion.l_le_l_iff GaloisCoinsertion.l_le_l_iff

theorem strictMono_l [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l :=
  fun _ _ h => gi.dual.strictMono_u h
#align galois_coinsertion.strict_mono_l GaloisCoinsertion.strictMono_l

theorem isGLB_of_l_image [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β}
    (hs : IsGLB (l '' s) a) : IsGLB s (u a) :=
  gi.dual.isLUB_of_u_image hs
#align galois_coinsertion.is_glb_of_l_image GaloisCoinsertion.isGLB_of_l_image

theorem isLUB_of_l_image [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {s : Set α} {a : β}
    (hs : IsLUB (l '' s) a) : IsLUB s (u a) :=
  gi.dual.isGLB_of_u_image hs
#align galois_coinsertion.is_lub_of_l_image GaloisCoinsertion.isLUB_of_l_image

section lift

variable [PartialOrder α]

-- Porting note: In `liftSemilatticeInf` and `liftSemilatticeSup` below, the elaborator
-- seems to struggle with αᵒᵈ vs α; the `by exact`s are not present in Lean 3, but without
-- them the declarations compile much more slowly for some reason.
-- Possibly related to the issue discussed at
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Performance.20issue.20with.20.60CompleteBooleanAlgebra.60/near/316760798

-- See note [reducible non instances]
/-- Lift the infima along a Galois coinsertion -/
abbrev liftSemilatticeInf [SemilatticeInf β] (gi : GaloisCoinsertion l u) : SemilatticeInf α :=
  { ‹PartialOrder α› with
    inf_le_left := fun a b => by
      exact (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_left a b
    inf_le_right := fun a b => by
      exact (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).inf_le_right a b
    le_inf := fun a b c => by
      exact (@OrderDual.instSemilatticeInf αᵒᵈ gi.dual.liftSemilatticeSup).le_inf a b c
    inf := fun a b => u (l a ⊓ l b) }
#align galois_coinsertion.lift_semilattice_inf GaloisCoinsertion.liftSemilatticeInf

-- See note [reducible non instances]
/-- Lift the suprema along a Galois coinsertion -/
abbrev liftSemilatticeSup [SemilatticeSup β] (gi : GaloisCoinsertion l u) : SemilatticeSup α :=
  { ‹PartialOrder α› with
    sup := fun a b =>
      gi.choice (l a ⊔ l b) <|
        sup_le (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_left)
          (gi.gc.monotone_l <| gi.gc.le_u <| le_sup_right)
    le_sup_left := fun a b => by
      exact (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_left a b
    le_sup_right := fun a b => by
      exact (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).le_sup_right a b
    sup_le := fun a b c => by
      exact (@OrderDual.instSemilatticeSup αᵒᵈ gi.dual.liftSemilatticeInf).sup_le a b c }
#align galois_coinsertion.lift_semilattice_sup GaloisCoinsertion.liftSemilatticeSup

-- See note [reducible non instances]
/-- Lift the suprema and infima along a Galois coinsertion -/
abbrev liftLattice [Lattice β] (gi : GaloisCoinsertion l u) : Lattice α :=
  { gi.liftSemilatticeSup, gi.liftSemilatticeInf with }
#align galois_coinsertion.lift_lattice GaloisCoinsertion.liftLattice

-- See note [reducible non instances]
/-- Lift the bot along a Galois coinsertion -/
abbrev liftOrderBot [Preorder β] [OrderBot β] (gi : GaloisCoinsertion l u) : OrderBot α :=
  { @OrderDual.instOrderBot _ _ gi.dual.liftOrderTop with bot := gi.choice ⊥ <| bot_le }
#align galois_coinsertion.lift_order_bot GaloisCoinsertion.liftOrderBot

-- See note [reducible non instances]
/-- Lift the top, bottom, suprema, and infima along a Galois coinsertion -/
abbrev liftBoundedOrder
    [Preorder β] [BoundedOrder β] (gi : GaloisCoinsertion l u) : BoundedOrder α :=
  { gi.liftOrderBot, gi.gc.liftOrderTop with }
#align galois_coinsertion.lift_bounded_order GaloisCoinsertion.liftBoundedOrder

-- See note [reducible non instances]
/-- Lift all suprema and infima along a Galois coinsertion -/
abbrev liftCompleteLattice [CompleteLattice β] (gi : GaloisCoinsertion l u) : CompleteLattice α :=
  { @OrderDual.instCompleteLattice αᵒᵈ gi.dual.liftCompleteLattice with
    sInf := fun s => u (sInf (l '' s))
    sSup := fun s => gi.choice (sSup (l '' s)) _ }
#align galois_coinsertion.lift_complete_lattice GaloisCoinsertion.liftCompleteLattice

end lift

end GaloisCoinsertion

/-- `sSup` and `Iic` form a Galois insertion. -/
def gi_sSup_Iic [CompleteSemilatticeSup α] :
    GaloisInsertion (sSup : Set α → α) (Iic : α → Set α) :=
  gc_sSup_Iic.toGaloisInsertion fun _ ↦ le_sSup le_rfl

/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion. -/
def gci_Ici_sInf [CompleteSemilatticeInf α] :
    GaloisCoinsertion (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α) :=
  gc_Ici_sInf.toGaloisCoinsertion fun _ ↦ sInf_le le_rfl

/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `WithBot.unbot' ⊥` and
coercion form a Galois insertion. -/
def WithBot.giUnbot'Bot [Preorder α] [OrderBot α] :
    GaloisInsertion (WithBot.unbot' ⊥) (some : α → WithBot α) where
  gc _ _ := WithBot.unbot'_le_iff (fun _ ↦ bot_le)
  le_l_u _ := le_rfl
  choice o _ := o.unbot' ⊥
  choice_eq _ _ := rfl
#align with_bot.gi_unbot'_bot WithBot.giUnbot'Bot
